Nuprl Definition : mk_oset 13,42
mk_oset(T;eq;leq) == <T, eq, leq> 
latex

Upsets 1
Wellformedness Lemmasmk oset wf

origin